/*
 * BFRMain.cpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#include <getopt.h>

#include <cassert>

#include <iostream>
#include <fstream>
#include <string>
#include <list>
#include <limits>
#include <utility>

// TODO: deprecated, but I think the newest version is not available everywhere...
// TODO: set types correctly. (tighten lp and stuff after style change)
#include <boost/timer.hpp>
#include <boost/lexical_cast.hpp>

#include "bfr/Clause.hpp"
#include "bfr/Literal.hpp"

#include "bfr/ClauseSet.hpp"
#include "bfr/OccurrencePattern.hpp"

#include "bfr/DIMACSParser.hpp"
#include "bfr/DIMACSCollectionParser.hpp"

#include "bfr/CoefficientType.hpp"
#include "bfr/LPB.hpp"
#include "bfr/LPBConversionException.hpp"
#include "bfr/BooleanVector.hpp"

#include "bfr/lpbCombinatorial/SolverInformation.hpp"
#include "bfr/lpbCombinatorial/SplittingTreeNode.hpp"
#include "bfr/lpbCombinatorial/SplittingTree.hpp"
#include "bfr/lpbCombinatorial/MinimumChooser.hpp"

#include "bfr/lpbCombinatorial/TreeToLPB.hpp"
#include "bfr/lpbCombinatorial/ExtendedTreeSolver.hpp"

#include "bfr/lpbLP/LPSolver.hpp"

using namespace std;
using namespace bfr;
using boost::timer;
using boost::lexical_cast;
using boost::bad_lexical_cast;


size_t compareCutTreeSavings(ClauseSet *cs, size_t size) {
    SplittingTree cutTree(cs, size);
    cutTree.createTree<true>(true, false);
    SplittingTree fullTree(cs, size);
    fullTree.createTree<false>(true, false);
    
    size_t difference = 0;
    
    while (size >= 0)
    {
        cout << "column " << size << ": cut " << cutTree.getContext()->getColumnSize(size)
        << " vs. full " << fullTree.getContext()->getColumnSize(size) << endl;
        
        difference += fullTree.getContext()->getColumnSize(size);
        difference -= cutTree.getContext()->getColumnSize(size);
        
        if (size > 0)
        {
            --size;
        }
        else
        {
            cout << "accumulated difference: " << difference << endl;
            return difference;
        }
    }
}

double runLPSolver(LPSolver &lpSolver, ClauseSet *cs) {
    timer t;
    double result = 0;
    try {
        LPB *lpb = lpSolver.convert(cs);
        result = t.elapsed();
        // lpb->sortCoefficients();
        cout << "LPB is: " << *lpb << std::endl;
        delete lpb;
    } catch (const LPBConversionException &e) {
        result = t.elapsed();
        // cout << "can't convert DNF to LPB. Error message:"
        //      << endl
        //      << e.what()
        //      << endl;
    }
    return result;
}

template<class TreeSolverT>
std::tuple<double,size_t,float> runTreeSolver(TreeSolverT &minSolver, size_t size,
                                     ClauseSet *cs, bool cutTree, bool symTest) {
  //std::cout << "call runTreeSolver" << std::endl;
    timer ti;
    size_t repairFlag;
    double result = 0;
    // start combinatorial solver
    SplittingTree t(cs, size);
    if (cutTree) {
        t.createTree<true>(symTest, false);
    }
    else {
        t.createTree<false>(symTest, false);
    }
    //cout << *t.getContext() << endl;//JGS commented out
    //cout << "Trying to convert: " << *cs << endl;
    //cout << "Trying: " << endl;
    //cs->writeDIMACS(cout);
    //cout << endl;
    //cout << "created" << endl;
    //ti.restart();
    try {
      //ti.restart();
        LPB *lpb = minSolver.solve(&t);
	result = ti.elapsed();
	repairFlag = minSolver.getRepairFlag();
	if (repairFlag == 1) {
	  //cout << "repair was used" << endl; 
	}
        // lpb->sortCoefficients();
        cout << "LPB is: " << *lpb << endl;
        delete lpb;
    } catch (const LPBConversionException &e) {
        cout << e.what() << endl;
        result = ti.elapsed();
	repairFlag = 2;
        cout << "Can't convert DNF to LPB. Error message:"
             << endl
             << e.what()
             << endl;
        //cout << *cs << endl;
        //cout << *t.getContext() << endl;//JGS commented out
    }
    // cout << "==================================" << endl;
    //cout << ((float)t.numFinalTrueNodes() / (float)t.getRoot()->getDNF()->size()) << " + ";
    return std::make_tuple(result,repairFlag,
			   ((float)t.numFinalTrueNodes() / (float)t.getRoot()->getDNF()->size()));
    //3rd arg: Symmetry saving: final true nodes / number of clauses
    //    return result;
}

// actually just for testing, nothing serious
int main(int argc, char** argv) {
    assert(numeric_limits<lpb_coefficient_t>::has_infinity);
    string version = "0.9.1";
    string url = "http://code.google.com/p/recognition-procedures-"
            "for-boolean-functions/";
    string progName = "boolean-function-recognition";
    string lpbConversionComb = "combinatorial";
    string lpbConversionLP = "lp";
    string TRUE_STRING = "true";
    string FALSE_STRING = "false";
    string ZERO_STRING = "0";
    string ONE_STRING = "1";
    string NONE_STR = "none";
    string NEIGHBOUR_STR = "neighbour";
    string ALL_STR = "all";
    string MIN_CHOOSER = "min";
    // 0 means linear program
    // 1 means combinatorial
    short lpbConversionMode = 0;
    //CoefficientChooser *chooser = new MinimumChooser();
    //SolverInformation *solverInf = new DoubleSolverInformation();
    //TreeToLPB *solver = new ClassicalTreeSolver(chooser, solverInf);

    DIMACSParser parser;

    const int maxID = CHAR_MAX;
    const int metaDimacsArg = maxID + 1;
    const int dimacsCArg = maxID + 2;
    const int lpbConversionArg = maxID + 3;
    const int lpbLPIntModeArg = maxID + 4;
    const int lpbLPTightenArg = maxID + 5;
    const int lpbRegTestArg = maxID + 6;
    const int cutTreeArg = maxID + 7;
    const int repairArg = maxID + 8;
    const int symmetryArg = maxID + 9;

    string dimacsMeta;
    bool lpbInt = true;
    LPSolver::tighten_lp tightenLP = LPSolver::tighten_lp::NEIGHBOURS;
    bool lpbRegTest = true;
    // TODO: buggy
    bool cutTree = false;
    bool repair = true;
    bool symmetryTest = true;
    //ClassicalTreeSolver<DoubleSolverInformation, MinimumChooser> classicalSolver;
    LPSolver lpSolver(lpbInt, tightenLP, lpbRegTest);

    TreeToLPB<MinimumChooser> minSolver;
    ExtendedTreeSolver<MinimumChooser> minRepairSolver;

    static struct option long_options[] = {
        {"help", no_argument, 0, 'h'},
        {"version", no_argument, 0, 'v'},
        {"dimacs", required_argument, 0, 'd'},
        {"dimacsM", required_argument, 0, metaDimacsArg},
        {"dimacsC", required_argument, 0, dimacsCArg},
        {"lpbConv", required_argument, 0, lpbConversionArg},
        {"lpbInt", required_argument, 0, lpbLPIntModeArg},
        {"lpTighten", required_argument, 0, lpbLPTightenArg},
        {"regTest", required_argument, 0, lpbRegTestArg},
        {"repair", required_argument, 0, repairArg},
        {"cutTree", required_argument, 0, cutTreeArg},
        {"symTest", required_argument, 0, symmetryArg},
        {0, 0, 0, 0}
    };

    int index = 0;
    int c;
    while ((c = getopt_long(argc, argv, "hvd:",
                     long_options, &index)) != -1) {
        switch (c) {
        case 0:
        case 1:
        case 2:
            // should not happen
            break;
        case 'h':
               cout << "Boolean function library"
                " (Boolean function recognition.)" << endl << endl
                    << "Use the \"--clauseSet\" option to define"
                    " clause sets (interpreted either as DNF or CNF)"
                    " depending on what you are planning to do with it."
                    << endl << endl
                    << "Use \"--dimacs\" to input a DIMACS CNF problem"
                    " from a file."<< endl
                    << "Use \"--dimacsM FILE\" to pass a meta file for a"
                    << " DIMACS collection and the collection itself with the "
                    << "command \"--dimacsC FILE\"." << endl
                    << "The meta file must contain the number of problems "
                    << "in the DIMACS collection." << endl;
            return 0;
        case 'v':
            cout << progName
                 << " (version "
                 << version
                 << ")"
                 << endl
                 << endl;
            cout << "See \""
                 << url
                 << "\" for more information."
                 << endl
                 << endl;
            cout << "Copyright (C) 2012 Fabian Wenzelmann, "
                 << "Christian Schilling, Jan-Georg Smaus" << std::endl;
            cout << "Published under the GPL version 3, "
                 << "see http://www.gnu.org/licenses/gpl-3.0.txt"
                 << std::endl;
            return 0;
        case 'd':
        {
            ifstream in;
            in.open(optarg);
            ClauseSet *cs;
            double passed;
            try {
                cs = parser.parse(in);
            } catch (string &e) {
                cerr << "Unable to parse input \"" << optarg
                          << "\" as DIMACS problem." << std::endl;
                cerr << "Error Message:" << std::endl;
                cerr << e << std::endl;
                return 1;
            }
            if (lpbConversionMode == 0) {
                // start LP solver
                LPSolver lpSolver(lpbInt, tightenLP, lpbRegTest);
                passed = runLPSolver(lpSolver, cs);
            }
            else if (lpbConversionMode == 1) {
	      //	        std::pair<double,size_t> result;
	        std::tuple<double,size_t,float> result;
                if (repair) {
                    result = runTreeSolver(minRepairSolver,parser.getVariableCount(), cs, cutTree, symmetryTest);
		    passed = std::get<0>(result);
		    //                    passed = runTreeSolver(minRepairSolver,parser.getVariableCount(), cs, cutTree, symmetryTest);
                }
                else {
                    result = runTreeSolver(minSolver, parser.getVariableCount(), cs, cutTree, symmetryTest);
		    passed = std::get<0>(result);
		    //  		    passed = runTreeSolver(minSolver, parser.getVariableCount(), cs, cutTree, symmetryTest);
                }
            }
            else {
                assert (false);
            }
            cout << "Finished after " << passed
                 << " seconds." << endl;
            delete cs;
            in.close();
            break;
        }

        case metaDimacsArg: {
            dimacsMeta = optarg;
            break;
        }

        case dimacsCArg: {
            if (dimacsMeta == "") {
                cerr << "Invalid DIMACS collection meta file. Forgot "
                     << "to set it with \"--dimacsM\"?" << std::endl;
                return 1;
            }
            size_t num;
            try {
                num = lexical_cast<size_t>(dimacsMeta);
            } catch (const boost::bad_lexical_cast &e ) {
                ifstream metaIn;
                metaIn.open(dimacsMeta.c_str());
                if (metaIn.bad()) {
                    cerr << "Unable to open DIMACS meta file \""
                         << dimacsMeta << "\"." << std::endl;
                    return 1;
                }
                metaIn >> num;
                metaIn.close();
            }
            ifstream in;
            in.open(optarg);

            if (in.bad()) {
                cerr << "Unable to open DIMACS collection file\""
                     << optarg << "\"." << std::endl;
                return 1;
            }

            DIMACSCollectionParser cParser(&in, num);

            double passed = 0;
            double passed_repair = 0;
	    size_t conv_fail = 0;
	    size_t repair_success = 0;
	    size_t nonrepair_success = 0;
	    //size_t cutTreeSavings = 0;
	    float cutTreeSavings = 0.0;

            for (DIMACSCollectionParser::const_iterator dit = cParser.begin();
                 dit < cParser.end();
                 dit++) {
	      //cout << endl << "Next problem" << endl;
                try {
                    pair<ClauseSet*, size_t> next = *dit;
                    ClauseSet *cs = next.first;
                    if (lpbConversionMode == 0) {
                        // start LP solver
                        LPSolver lpSolver(lpbInt, tightenLP, lpbRegTest);
                        passed += runLPSolver(lpSolver, cs);
			nonrepair_success++;
                    }
                    else if (lpbConversionMode == 1) {
		      //cutTreeSavings += compareCutTreeSavings(cs, next.second);
                    
		        std::tuple<double,size_t,float> result;
                        if (repair) {
                            result = runTreeSolver(minRepairSolver,next.second,cs, cutTree, symmetryTest);
			    //cout << "result.second = " << std::get<1>(result) << endl;
			    if (std::get<1>(result) == 2)//conversion failed
			      {
				conv_fail++;
			      } 
                            else 
			      {
				if (std::get<1>(result) == 1)//repair was used
				  {
				    //cout << "passed_repair += " << endl;
				    passed_repair += std::get<0>(result);
				    repair_success++;
				  } else//repair was not used
				  { 
				    //cout << "passed += " << endl;
				    passed += std::get<0>(result);
				    nonrepair_success++;
				  }
			      }
			    //			  passed += runTreeSolver(minRepairSolver,next.second, cs, cutTree, symmetryTest);
                        }
                        else {
			    result = runTreeSolver(minSolver, next.second, cs, cutTree, symmetryTest);
			    passed += std::get<0>(result);
			    nonrepair_success++;
			    //			  passed += runTreeSolver(minSolver, next.second, cs, cutTree, symmetryTest);
                        }
			//cout << "cutTree Savings = " << std::get<2>(result) << endl;
			cutTreeSavings += std::get<2>(result);
                    }
                    else {
                        assert (false);
                    }
                    delete cs;
                }
                catch (const string &error) {
                    cerr << "Error parsing DIMACS collection \""
                         << optarg << "\". Error message:" << std::endl
                         << error << std::endl;
                    return 1;
                }
            }
	    cout << conv_fail + repair_success + nonrepair_success << " problems in total" << endl;
	    cout << "Failed on " << conv_fail << ", i.e. " 
		 << ((float)conv_fail / (float)(conv_fail + repair_success + nonrepair_success)) * 100.0 
		 << "% of the problems." << endl;
            cout << "Succeeded without repair: " << nonrepair_success 
		 << ". " << ((float)nonrepair_success / (float)(conv_fail + repair_success + nonrepair_success)) * 100.0
		 << "%. Average runtime " << 1000 * (passed / nonrepair_success) << " milliseconds." << endl ;
            cout << "Succeeded with repair: " << repair_success 
		 << ". " << ((float)repair_success / (float)(conv_fail + repair_success + nonrepair_success)) * 100.0
		 << "%. Average runtime " << 1000 * (passed_repair / repair_success) << " milliseconds." << endl;
            cout << "Average runtime for all successful runs: " << 
	      1000 * ((passed + passed_repair) / (nonrepair_success + repair_success)) <<
	      " milliseconds." << endl;
	    cout << "Relative tree size with cutTree compared to without cutTree = no. of true final nodes / number of clauses: " 
		 << (cutTreeSavings / (float)(conv_fail + repair_success + nonrepair_success))  * 100.0 << endl;
            break;
        }
        case lpbConversionArg: {
            if (lpbConversionLP == optarg) {
                lpbConversionMode = 0;
            }
            else if (lpbConversionComb == optarg) {
                lpbConversionMode = 1;
            }
            else {
                cerr << "Unknown LPB conversion mode \"" << optarg
                     << "\". Allowed values are \"" << lpbConversionLP
                     << "\" and \"" << lpbConversionComb << "\"."
                     << std::endl;
                return 1;
            }
            break;
        }
        case lpbLPIntModeArg: {
            if ((TRUE_STRING == optarg) || ONE_STRING == optarg) {
                lpbInt = true;
            }
            else if ((FALSE_STRING == optarg) || (ZERO_STRING == optarg)) {
                lpbInt = false;
            }
            else {
                cerr << "Invalid lpbIntMode: \"" << optarg
                     << "\". must be \"true\" or \"false\".";
                return 1;
            }
            break;
        }
        case lpbLPTightenArg: {
            if (NONE_STR == optarg) {
                tightenLP = LPSolver::tighten_lp::NONE;
            }
            else if (NEIGHBOUR_STR == optarg) {
                tightenLP = LPSolver::tighten_lp::NEIGHBOURS;
            }
            else if (ALL_STR == optarg) {
                tightenLP = LPSolver::tighten_lp::ALL;
            }
            else {
                cerr << "Unknown lp tighten type \"" << optarg
                     << "\". Valid options are:" << std::endl
                     << "\t\"" << NONE_STR << "\"" << std::endl
                     << "\t\"" << NEIGHBOUR_STR << "\"" << std::endl
                     << "\t\"" << ALL_STR << "\"" << std::endl;
                return 1;
            }
            break;
        }

        case lpbRegTestArg: {
            if ((TRUE_STRING == optarg) || ONE_STRING == optarg) {
                lpbRegTest = true;
            }
            else if ((FALSE_STRING == optarg) || (ZERO_STRING == optarg)) {
                lpbRegTest = false;
            }
            else {
                cerr << "Invalid Regular test option: \"" << optarg
                     << "\". must be \"true\" or \"false\"."
                     << endl
                     << "WARNING: Not supported yet, value will be ignored."
                     << endl;
                return 1;
            }
            break;
        }
        case cutTreeArg: {
            if ((TRUE_STRING == optarg) || (ONE_STRING == optarg)) {
                cutTree = true;
            }
            else if ((FALSE_STRING == optarg) || (ZERO_STRING == optarg)) {
                cutTree = false;
            }
            else {
                cerr << "Invalid cut tree option: \"" << optarg
                     << "\". must be \"true\" or \"false\"."
                     << std::endl;
                return 1;
            }
            break;
        }
        case repairArg: {
            if ((TRUE_STRING == optarg) || ONE_STRING == optarg) {
                repair = true;
            }
            else if ((FALSE_STRING == optarg) || (ZERO_STRING == optarg)) {
                repair = false;
            }
            break;
        }
        case symmetryArg: {
            if ((TRUE_STRING == optarg) || ONE_STRING == optarg) {
                symmetryTest = true;
            }
            else if ((FALSE_STRING == optarg) || (ZERO_STRING == optarg)) {
                symmetryTest = false;
            }
            break;
        }
        case '?':
            break;
        }
    }
    return 0;
}
